H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 2.207 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ LR

mainModule Main

((basicIORun :: IO a -> IOFinished a) :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\x→Hugs_Catch (a x) f1 f2 s

is transformed to

hugs_catch0 a f1 f2 s x = Hugs_Catch (a x) f1 f2 s

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

mainModule Main

((basicIORun :: IO a -> IOFinished a) :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Case Reductions:
The following Case expression

case primCatchException (catch' m) of
Left exn → f1 exn

Right (Hugs_Return a) → s a

Right (Hugs_Error e) → f2 e

Right (Hugs_ForkThread a b) → Hugs_ForkThread (Hugs_Catch a f1 f2 s) b

Right (Hugs_YieldThread a) → Hugs_YieldThread (Hugs_Catch a f1 f2 s)

Right (Hugs_BlockThread a b) → Hugs_BlockThread (hugs_catch0 a f1 f2 s) b

Right r → r

is transformed to

hugs_catch1 f1 s f2 (Left exn) = f1 exn

hugs_catch1 f1 s f2 (Right (Hugs_Return a)) = s a

hugs_catch1 f1 s f2 (Right (Hugs_Error e)) = f2 e

hugs_catch1 f1 s f2 (Right (Hugs_ForkThread a b)) = Hugs_ForkThread (Hugs_Catch a f1 f2 s) b

hugs_catch1 f1 s f2 (Right (Hugs_YieldThread a)) = Hugs_YieldThread (Hugs_Catch a f1 f2 s)

hugs_catch1 f1 s f2 (Right (Hugs_BlockThread a b)) = Hugs_BlockThread (hugs_catch0 a f1 f2 s) b

hugs_catch1 f1 s f2 (Right r) = r

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

mainModule Main

((basicIORun :: IO a -> IOFinished a) :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((basicIORun :: IO a -> IOFinished a) :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((basicIORun :: IO a -> IOFinished a) :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

hugs_catch1 f1 s f2 (primCatchException (catch' m))

where

catch' (Hugs_Catch m' f1' f2' s') = catch' (hugs_catch m' f1' f2' s')

catch' x = x

hugs_catch0 a f1 f2 s x = Hugs_Catch (a x) f1 f2 s

hugs_catch1 f1 s f2 (Left exn) = f1 exn

hugs_catch1 f1 s f2 (Right (Hugs_Return a)) = s a

hugs_catch1 f1 s f2 (Right (Hugs_Error e)) = f2 e

hugs_catch1 f1 s f2 (Right (Hugs_ForkThread a b)) = Hugs_ForkThread (Hugs_Catch a f1 f2 s) b

hugs_catch1 f1 s f2 (Right (Hugs_YieldThread a)) = Hugs_YieldThread (Hugs_Catch a f1 f2 s)

hugs_catch1 f1 s f2 (Right (Hugs_BlockThread a b)) = Hugs_BlockThread (hugs_catch0 a f1 f2 s) b

hugs_catch1 f1 s f2 (Right r) = r

are unpacked to the following functions on top level

hugs_catchCatch' (Hugs_Catch m' f1' f2' s') = hugs_catchCatch' (hugs_catch m' f1' f2' s')

hugs_catchCatch' x = x

hugs_catchHugs_catch0 a f1 f2 s x = Hugs_Catch (a x) f1 f2 s

hugs_catchHugs_catch1 f1 s f2 (Left exn) = f1 exn

hugs_catchHugs_catch1 f1 s f2 (Right (Hugs_Return a)) = s a

hugs_catchHugs_catch1 f1 s f2 (Right (Hugs_Error e)) = f2 e

hugs_catchHugs_catch1 f1 s f2 (Right (Hugs_ForkThread a b)) = Hugs_ForkThread (Hugs_Catch a f1 f2 s) b

hugs_catchHugs_catch1 f1 s f2 (Right (Hugs_YieldThread a)) = Hugs_YieldThread (Hugs_Catch a f1 f2 s)

hugs_catchHugs_catch1 f1 s f2 (Right (Hugs_BlockThread a b)) = Hugs_BlockThread (hugs_catchHugs_catch0 a f1 f2 s) b

hugs_catchHugs_catch1 f1 s f2 (Right r) = r

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                      ↳ Narrow

mainModule Main

(basicIORun :: IO a -> IOFinished a)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="basicIORun",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="basicIORun wu3",fontsize=16,color="burlywood",shape="triangle"];401[label="wu3/IO wu30",fontsize=10,color="white",style="solid",shape="box"];3 -> 401[label="",style="solid", color="burlywood", weight=9];
401 -> 4[label="",style="solid", color="burlywood", weight=3];
4[label="basicIORun (IO wu30)",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5 -> 237[label="",style="dashed", color="red", weight=0];
5[label="loop (wu30 Hugs_Error (Hugs_Return . toObj) : [])",fontsize=16,color="magenta"];5 -> 238[label="",style="dashed", color="magenta", weight=3];
5 -> 239[label="",style="dashed", color="magenta", weight=3];
238[label="[]",fontsize=16,color="green",shape="box"];239[label="wu30 Hugs_Error (Hugs_Return . toObj)",fontsize=16,color="green",shape="box"];239 -> 314[label="",style="dashed", color="green", weight=3];
239 -> 315[label="",style="dashed", color="green", weight=3];
237[label="loop (wu8 : wu9)",fontsize=16,color="burlywood",shape="triangle"];403[label="wu8/Hugs_ExitWith wu80",fontsize=10,color="white",style="solid",shape="box"];237 -> 403[label="",style="solid", color="burlywood", weight=9];
403 -> 316[label="",style="solid", color="burlywood", weight=3];
404[label="wu8/Hugs_Error wu80",fontsize=10,color="white",style="solid",shape="box"];237 -> 404[label="",style="solid", color="burlywood", weight=9];
404 -> 317[label="",style="solid", color="burlywood", weight=3];
405[label="wu8/Hugs_Catch wu80 wu81 wu82 wu83",fontsize=10,color="white",style="solid",shape="box"];237 -> 405[label="",style="solid", color="burlywood", weight=9];
405 -> 318[label="",style="solid", color="burlywood", weight=3];
406[label="wu8/Hugs_ForkThread wu80 wu81",fontsize=10,color="white",style="solid",shape="box"];237 -> 406[label="",style="solid", color="burlywood", weight=9];
406 -> 319[label="",style="solid", color="burlywood", weight=3];
407[label="wu8/Hugs_DeadThread",fontsize=10,color="white",style="solid",shape="box"];237 -> 407[label="",style="solid", color="burlywood", weight=9];
407 -> 320[label="",style="solid", color="burlywood", weight=3];
408[label="wu8/Hugs_YieldThread wu80",fontsize=10,color="white",style="solid",shape="box"];237 -> 408[label="",style="solid", color="burlywood", weight=9];
408 -> 321[label="",style="solid", color="burlywood", weight=3];
409[label="wu8/Hugs_Return wu80",fontsize=10,color="white",style="solid",shape="box"];237 -> 409[label="",style="solid", color="burlywood", weight=9];
409 -> 322[label="",style="solid", color="burlywood", weight=3];
410[label="wu8/Hugs_BlockThread wu80 wu81",fontsize=10,color="white",style="solid",shape="box"];237 -> 410[label="",style="solid", color="burlywood", weight=9];
410 -> 323[label="",style="solid", color="burlywood", weight=3];
314[label="Hugs_Error",fontsize=16,color="green",shape="box"];315[label="Hugs_Return . toObj",fontsize=16,color="grey",shape="box"];315 -> 324[label="",style="dashed", color="grey", weight=3];
316[label="loop (Hugs_ExitWith wu80 : wu9)",fontsize=16,color="black",shape="box"];316 -> 325[label="",style="solid", color="black", weight=3];
317[label="loop (Hugs_Error wu80 : wu9)",fontsize=16,color="black",shape="box"];317 -> 326[label="",style="solid", color="black", weight=3];
318[label="loop (Hugs_Catch wu80 wu81 wu82 wu83 : wu9)",fontsize=16,color="black",shape="box"];318 -> 327[label="",style="solid", color="black", weight=3];
319[label="loop (Hugs_ForkThread wu80 wu81 : wu9)",fontsize=16,color="black",shape="box"];319 -> 328[label="",style="solid", color="black", weight=3];
320[label="loop (Hugs_DeadThread : wu9)",fontsize=16,color="black",shape="box"];320 -> 329[label="",style="solid", color="black", weight=3];
321[label="loop (Hugs_YieldThread wu80 : wu9)",fontsize=16,color="black",shape="box"];321 -> 330[label="",style="solid", color="black", weight=3];
322[label="loop (Hugs_Return wu80 : wu9)",fontsize=16,color="burlywood",shape="box"];411[label="wu9/wu90 : wu91",fontsize=10,color="white",style="solid",shape="box"];322 -> 411[label="",style="solid", color="burlywood", weight=9];
411 -> 331[label="",style="solid", color="burlywood", weight=3];
412[label="wu9/[]",fontsize=10,color="white",style="solid",shape="box"];322 -> 412[label="",style="solid", color="burlywood", weight=9];
412 -> 332[label="",style="solid", color="burlywood", weight=3];
323[label="loop (Hugs_BlockThread wu80 wu81 : wu9)",fontsize=16,color="black",shape="box"];323 -> 333[label="",style="solid", color="black", weight=3];
324[label="Hugs_Return . toObj",fontsize=16,color="black",shape="triangle"];324 -> 334[label="",style="solid", color="black", weight=3];
325[label="Finished_ExitWith wu80",fontsize=16,color="green",shape="box"];326[label="Finished_Error wu80",fontsize=16,color="green",shape="box"];327 -> 237[label="",style="dashed", color="red", weight=0];
327[label="loop (hugs_catch wu80 wu81 wu82 wu83 : wu9)",fontsize=16,color="magenta"];327 -> 335[label="",style="dashed", color="magenta", weight=3];
328 -> 237[label="",style="dashed", color="red", weight=0];
328[label="loop (wu80 : wu81 : wu9)",fontsize=16,color="magenta"];328 -> 336[label="",style="dashed", color="magenta", weight=3];
328 -> 337[label="",style="dashed", color="magenta", weight=3];
329[label="loop wu9",fontsize=16,color="burlywood",shape="triangle"];415[label="wu9/wu90 : wu91",fontsize=10,color="white",style="solid",shape="box"];329 -> 415[label="",style="solid", color="burlywood", weight=9];
415 -> 338[label="",style="solid", color="burlywood", weight=3];
416[label="wu9/[]",fontsize=10,color="white",style="solid",shape="box"];329 -> 416[label="",style="solid", color="burlywood", weight=9];
416 -> 339[label="",style="solid", color="burlywood", weight=3];
330 -> 329[label="",style="dashed", color="red", weight=0];
330[label="loop (wu9 ++ wu80 : [])",fontsize=16,color="magenta"];330 -> 340[label="",style="dashed", color="magenta", weight=3];
331[label="loop (Hugs_Return wu80 : wu90 : wu91)",fontsize=16,color="black",shape="box"];331 -> 341[label="",style="solid", color="black", weight=3];
332[label="loop (Hugs_Return wu80 : [])",fontsize=16,color="black",shape="box"];332 -> 342[label="",style="solid", color="black", weight=3];
333 -> 329[label="",style="dashed", color="red", weight=0];
333[label="loop (wu81 wu80 : wu9)",fontsize=16,color="magenta"];333 -> 343[label="",style="dashed", color="magenta", weight=3];
334[label="Hugs_Return (toObj wu10)",fontsize=16,color="green",shape="box"];334 -> 344[label="",style="dashed", color="green", weight=3];
335[label="hugs_catch wu80 wu81 wu82 wu83",fontsize=16,color="black",shape="triangle"];335 -> 345[label="",style="solid", color="black", weight=3];
336[label="wu81 : wu9",fontsize=16,color="green",shape="box"];337[label="wu80",fontsize=16,color="green",shape="box"];338[label="loop (wu90 : wu91)",fontsize=16,color="burlywood",shape="box"];419[label="wu90/Hugs_ExitWith wu900",fontsize=10,color="white",style="solid",shape="box"];338 -> 419[label="",style="solid", color="burlywood", weight=9];
419 -> 346[label="",style="solid", color="burlywood", weight=3];
420[label="wu90/Hugs_Error wu900",fontsize=10,color="white",style="solid",shape="box"];338 -> 420[label="",style="solid", color="burlywood", weight=9];
420 -> 347[label="",style="solid", color="burlywood", weight=3];
421[label="wu90/Hugs_Catch wu900 wu901 wu902 wu903",fontsize=10,color="white",style="solid",shape="box"];338 -> 421[label="",style="solid", color="burlywood", weight=9];
421 -> 348[label="",style="solid", color="burlywood", weight=3];
422[label="wu90/Hugs_ForkThread wu900 wu901",fontsize=10,color="white",style="solid",shape="box"];338 -> 422[label="",style="solid", color="burlywood", weight=9];
422 -> 349[label="",style="solid", color="burlywood", weight=3];
423[label="wu90/Hugs_DeadThread",fontsize=10,color="white",style="solid",shape="box"];338 -> 423[label="",style="solid", color="burlywood", weight=9];
423 -> 350[label="",style="solid", color="burlywood", weight=3];
424[label="wu90/Hugs_YieldThread wu900",fontsize=10,color="white",style="solid",shape="box"];338 -> 424[label="",style="solid", color="burlywood", weight=9];
424 -> 351[label="",style="solid", color="burlywood", weight=3];
425[label="wu90/Hugs_Return wu900",fontsize=10,color="white",style="solid",shape="box"];338 -> 425[label="",style="solid", color="burlywood", weight=9];
425 -> 352[label="",style="solid", color="burlywood", weight=3];
426[label="wu90/Hugs_BlockThread wu900 wu901",fontsize=10,color="white",style="solid",shape="box"];338 -> 426[label="",style="solid", color="burlywood", weight=9];
426 -> 353[label="",style="solid", color="burlywood", weight=3];
339[label="loop []",fontsize=16,color="black",shape="box"];339 -> 354[label="",style="solid", color="black", weight=3];
340[label="wu9 ++ wu80 : []",fontsize=16,color="burlywood",shape="triangle"];427[label="wu9/wu90 : wu91",fontsize=10,color="white",style="solid",shape="box"];340 -> 427[label="",style="solid", color="burlywood", weight=9];
427 -> 355[label="",style="solid", color="burlywood", weight=3];
428[label="wu9/[]",fontsize=10,color="white",style="solid",shape="box"];340 -> 428[label="",style="solid", color="burlywood", weight=9];
428 -> 356[label="",style="solid", color="burlywood", weight=3];
341 -> 329[label="",style="dashed", color="red", weight=0];
341[label="loop ((wu90 : wu91) ++ Hugs_Return wu80 : [])",fontsize=16,color="magenta"];341 -> 357[label="",style="dashed", color="magenta", weight=3];
342[label="Finished_Return (fromObj wu80)",fontsize=16,color="green",shape="box"];342 -> 358[label="",style="dashed", color="green", weight=3];
343[label="wu81 wu80 : wu9",fontsize=16,color="green",shape="box"];343 -> 359[label="",style="dashed", color="green", weight=3];
344[label="toObj wu10",fontsize=16,color="black",shape="triangle"];344 -> 360[label="",style="solid", color="black", weight=3];
345[label="hugs_catchHugs_catch1 wu81 wu83 wu82 (primCatchException (hugs_catchCatch' wu80))",fontsize=16,color="black",shape="triangle"];345 -> 361[label="",style="solid", color="black", weight=3];
346[label="loop (Hugs_ExitWith wu900 : wu91)",fontsize=16,color="black",shape="box"];346 -> 362[label="",style="solid", color="black", weight=3];
347[label="loop (Hugs_Error wu900 : wu91)",fontsize=16,color="black",shape="box"];347 -> 363[label="",style="solid", color="black", weight=3];
348[label="loop (Hugs_Catch wu900 wu901 wu902 wu903 : wu91)",fontsize=16,color="black",shape="box"];348 -> 364[label="",style="solid", color="black", weight=3];
349[label="loop (Hugs_ForkThread wu900 wu901 : wu91)",fontsize=16,color="black",shape="box"];349 -> 365[label="",style="solid", color="black", weight=3];
350[label="loop (Hugs_DeadThread : wu91)",fontsize=16,color="black",shape="box"];350 -> 366[label="",style="solid", color="black", weight=3];
351[label="loop (Hugs_YieldThread wu900 : wu91)",fontsize=16,color="black",shape="box"];351 -> 367[label="",style="solid", color="black", weight=3];
352[label="loop (Hugs_Return wu900 : wu91)",fontsize=16,color="burlywood",shape="box"];430[label="wu91/wu910 : wu911",fontsize=10,color="white",style="solid",shape="box"];352 -> 430[label="",style="solid", color="burlywood", weight=9];
430 -> 368[label="",style="solid", color="burlywood", weight=3];
431[label="wu91/[]",fontsize=10,color="white",style="solid",shape="box"];352 -> 431[label="",style="solid", color="burlywood", weight=9];
431 -> 369[label="",style="solid", color="burlywood", weight=3];
353[label="loop (Hugs_BlockThread wu900 wu901 : wu91)",fontsize=16,color="black",shape="box"];353 -> 370[label="",style="solid", color="black", weight=3];
354[label="error []",fontsize=16,color="black",shape="box"];354 -> 371[label="",style="solid", color="black", weight=3];
355[label="(wu90 : wu91) ++ wu80 : []",fontsize=16,color="black",shape="box"];355 -> 372[label="",style="solid", color="black", weight=3];
356[label="[] ++ wu80 : []",fontsize=16,color="black",shape="box"];356 -> 373[label="",style="solid", color="black", weight=3];
357 -> 340[label="",style="dashed", color="red", weight=0];
357[label="(wu90 : wu91) ++ Hugs_Return wu80 : []",fontsize=16,color="magenta"];357 -> 374[label="",style="dashed", color="magenta", weight=3];
357 -> 375[label="",style="dashed", color="magenta", weight=3];
358[label="fromObj wu80",fontsize=16,color="black",shape="triangle"];358 -> 376[label="",style="solid", color="black", weight=3];
359[label="wu81 wu80",fontsize=16,color="green",shape="box"];359 -> 377[label="",style="dashed", color="green", weight=3];
360 -> 344[label="",style="dashed", color="red", weight=0];
360[label="toObj wu10",fontsize=16,color="magenta"];361 -> 345[label="",style="dashed", color="red", weight=0];
361[label="hugs_catchHugs_catch1 wu81 wu83 wu82 (primCatchException (hugs_catchCatch' wu80))",fontsize=16,color="magenta"];362[label="Finished_ExitWith wu900",fontsize=16,color="green",shape="box"];363[label="Finished_Error wu900",fontsize=16,color="green",shape="box"];364 -> 329[label="",style="dashed", color="red", weight=0];
364[label="loop (hugs_catch wu900 wu901 wu902 wu903 : wu91)",fontsize=16,color="magenta"];364 -> 378[label="",style="dashed", color="magenta", weight=3];
365 -> 329[label="",style="dashed", color="red", weight=0];
365[label="loop (wu900 : wu901 : wu91)",fontsize=16,color="magenta"];365 -> 379[label="",style="dashed", color="magenta", weight=3];
366 -> 329[label="",style="dashed", color="red", weight=0];
366[label="loop wu91",fontsize=16,color="magenta"];366 -> 380[label="",style="dashed", color="magenta", weight=3];
367 -> 329[label="",style="dashed", color="red", weight=0];
367[label="loop (wu91 ++ wu900 : [])",fontsize=16,color="magenta"];367 -> 381[label="",style="dashed", color="magenta", weight=3];
368[label="loop (Hugs_Return wu900 : wu910 : wu911)",fontsize=16,color="black",shape="box"];368 -> 382[label="",style="solid", color="black", weight=3];
369[label="loop (Hugs_Return wu900 : [])",fontsize=16,color="black",shape="box"];369 -> 383[label="",style="solid", color="black", weight=3];
370 -> 329[label="",style="dashed", color="red", weight=0];
370[label="loop (wu901 wu900 : wu91)",fontsize=16,color="magenta"];370 -> 384[label="",style="dashed", color="magenta", weight=3];
371[label="error []",fontsize=16,color="red",shape="box"];372[label="wu90 : wu91 ++ wu80 : []",fontsize=16,color="green",shape="box"];372 -> 385[label="",style="dashed", color="green", weight=3];
373[label="wu80 : []",fontsize=16,color="green",shape="box"];374[label="wu90 : wu91",fontsize=16,color="green",shape="box"];375[label="Hugs_Return wu80",fontsize=16,color="green",shape="box"];376 -> 358[label="",style="dashed", color="red", weight=0];
376[label="fromObj wu80",fontsize=16,color="magenta"];377[label="wu80",fontsize=16,color="green",shape="box"];378[label="hugs_catch wu900 wu901 wu902 wu903 : wu91",fontsize=16,color="green",shape="box"];378 -> 386[label="",style="dashed", color="green", weight=3];
379[label="wu900 : wu901 : wu91",fontsize=16,color="green",shape="box"];380[label="wu91",fontsize=16,color="green",shape="box"];381 -> 340[label="",style="dashed", color="red", weight=0];
381[label="wu91 ++ wu900 : []",fontsize=16,color="magenta"];381 -> 387[label="",style="dashed", color="magenta", weight=3];
381 -> 388[label="",style="dashed", color="magenta", weight=3];
382 -> 329[label="",style="dashed", color="red", weight=0];
382[label="loop ((wu910 : wu911) ++ Hugs_Return wu900 : [])",fontsize=16,color="magenta"];382 -> 389[label="",style="dashed", color="magenta", weight=3];
383[label="Finished_Return (fromObj wu900)",fontsize=16,color="green",shape="box"];383 -> 390[label="",style="dashed", color="green", weight=3];
384[label="wu901 wu900 : wu91",fontsize=16,color="green",shape="box"];384 -> 391[label="",style="dashed", color="green", weight=3];
385 -> 340[label="",style="dashed", color="red", weight=0];
385[label="wu91 ++ wu80 : []",fontsize=16,color="magenta"];385 -> 392[label="",style="dashed", color="magenta", weight=3];
386 -> 335[label="",style="dashed", color="red", weight=0];
386[label="hugs_catch wu900 wu901 wu902 wu903",fontsize=16,color="magenta"];386 -> 393[label="",style="dashed", color="magenta", weight=3];
386 -> 394[label="",style="dashed", color="magenta", weight=3];
386 -> 395[label="",style="dashed", color="magenta", weight=3];
386 -> 396[label="",style="dashed", color="magenta", weight=3];
387[label="wu91",fontsize=16,color="green",shape="box"];388[label="wu900",fontsize=16,color="green",shape="box"];389 -> 340[label="",style="dashed", color="red", weight=0];
389[label="(wu910 : wu911) ++ Hugs_Return wu900 : []",fontsize=16,color="magenta"];389 -> 397[label="",style="dashed", color="magenta", weight=3];
389 -> 398[label="",style="dashed", color="magenta", weight=3];
390 -> 358[label="",style="dashed", color="red", weight=0];
390[label="fromObj wu900",fontsize=16,color="magenta"];390 -> 399[label="",style="dashed", color="magenta", weight=3];
391[label="wu901 wu900",fontsize=16,color="green",shape="box"];391 -> 400[label="",style="dashed", color="green", weight=3];
392[label="wu91",fontsize=16,color="green",shape="box"];393[label="wu903",fontsize=16,color="green",shape="box"];394[label="wu901",fontsize=16,color="green",shape="box"];395[label="wu900",fontsize=16,color="green",shape="box"];396[label="wu902",fontsize=16,color="green",shape="box"];397[label="wu910 : wu911",fontsize=16,color="green",shape="box"];398[label="Hugs_Return wu900",fontsize=16,color="green",shape="box"];399[label="wu900",fontsize=16,color="green",shape="box"];400[label="wu900",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ NonTerminationProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_toObj(wu10, ba) → new_toObj(wu10, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_toObj(wu10, ba) → new_toObj(wu10, ba)

The TRS R consists of the following rules:none

s = new_toObj(wu10, ba) evaluates to t =new_toObj(wu10, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_toObj(wu10, ba) to new_toObj(wu10, ba).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ NonTerminationProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_fromObj(wu80, ba) → new_fromObj(wu80, ba)

The TRS R consists of the following rules:none

s = new_fromObj(wu80, ba) evaluates to t =new_fromObj(wu80, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_fromObj(wu80, ba) to new_fromObj(wu80, ba).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(wu90, wu91), wu80) → new_psPs(wu91, wu80)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(wu90, wu91), wu80) → new_psPs(wu91, wu80)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ NonTerminationProof

                          ↳ QDP

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80) → new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80)

The TRS R consists of the following rules:none

s = new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80) evaluates to t =new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80) to new_hugs_catchHugs_catch1(wu81, wu83, wu82, wu80).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop(ba) → new_loop(ba)

The TRS R consists of the following rules:

new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)
new_hugs_catch(wu80, wu81, wu82, wu83) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)
new_psPs0([], wu80) → :(wu80, [])
new_psPs0(:(wu90, wu91), wu80) → :(wu90, new_psPs0(wu91, wu80))

The set Q consists of the following terms:

new_psPs0([], x0)
new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)
new_psPs0(:(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop(ba) → new_loop(ba)

R is empty.
The set Q consists of the following terms:

new_psPs0([], x0)
new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)
new_psPs0(:(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_psPs0([], x0)
new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)
new_psPs0(:(x0, x1), x2)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ UsableRulesProof

                              ↳ QDP

                                ↳ QReductionProof

                                  ↳ QDP

                                    ↳ NonTerminationProof

                          ↳ QDP

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop(ba) → new_loop(ba)

The TRS R consists of the following rules:none

s = new_loop(ba) evaluates to t =new_loop(ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_loop(ba) to new_loop(ba).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop0(Hugs_Catch(wu80, wu81, wu82, wu83), wu9, ba) → new_loop0(new_hugs_catch(wu80, wu81, wu82, wu83), wu9, ba)
new_loop0(Hugs_ForkThread(wu80, wu81), wu9, ba) → new_loop0(wu80, :(wu81, wu9), ba)

The TRS R consists of the following rules:

new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)
new_hugs_catch(wu80, wu81, wu82, wu83) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)

The set Q consists of the following terms:

new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop0(Hugs_ForkThread(wu80, wu81), wu9, ba) → new_loop0(wu80, :(wu81, wu9), ba)

The TRS R consists of the following rules:

new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)
new_hugs_catch(wu80, wu81, wu82, wu83) → new_hugs_catchHugs_catch10(wu81, wu83, wu82, wu80)

The set Q consists of the following terms:

new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop0(Hugs_ForkThread(wu80, wu81), wu9, ba) → new_loop0(wu80, :(wu81, wu9), ba)

R is empty.
The set Q consists of the following terms:

new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_hugs_catch(x0, x1, x2, x3)
new_hugs_catchHugs_catch10(x0, x1, x2, x3)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ QDPSizeChangeProof

                      ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_loop0(Hugs_ForkThread(wu80, wu81), wu9, ba) → new_loop0(wu80, :(wu81, wu9), ba)

From the DPs we obtained the following set of size-change graphs:

new_loop0(Hugs_ForkThread(wu80, wu81), wu9, ba) → new_loop0(wu80, :(wu81, wu9), ba)
The graph contains the following edges 1 > 1, 3 >= 3

Haskell To QDPs

case	primCatchException (catch' m) of
	Left exn	→ f1 exn
	Right (Hugs_Return a)	→ s a
	Right (Hugs_Error e)	→ f2 e
	Right (Hugs_ForkThread a b)	→ Hugs_ForkThread (Hugs_Catch a f1 f2 s) b
	Right (Hugs_YieldThread a)	→ Hugs_YieldThread (Hugs_Catch a f1 f2 s)
	Right (Hugs_BlockThread a b)	→ Hugs_BlockThread (hugs_catch0 a f1 f2 s) b
	Right r	→ r

hugs_catch1	f1 s f2 (Left exn)	= f1 exn
hugs_catch1	f1 s f2 (Right (Hugs_Return a))	= s a
hugs_catch1	f1 s f2 (Right (Hugs_Error e))	= f2 e
hugs_catch1	f1 s f2 (Right (Hugs_ForkThread a b))	= Hugs_ForkThread (Hugs_Catch a f1 f2 s) b
hugs_catch1	f1 s f2 (Right (Hugs_YieldThread a))	= Hugs_YieldThread (Hugs_Catch a f1 f2 s)
hugs_catch1	f1 s f2 (Right (Hugs_BlockThread a b))	= Hugs_BlockThread (hugs_catch0 a f1 f2 s) b
hugs_catch1	f1 s f2 (Right r)	= r

hugs_catchCatch'	(Hugs_Catch m' f1' f2' s')	= hugs_catchCatch' (hugs_catch m' f1' f2' s')
hugs_catchCatch'	x	= x

hugs_catchHugs_catch1	f1 s f2 (Left exn)	= f1 exn
hugs_catchHugs_catch1	f1 s f2 (Right (Hugs_Return a))	= s a
hugs_catchHugs_catch1	f1 s f2 (Right (Hugs_Error e))	= f2 e
hugs_catchHugs_catch1	f1 s f2 (Right (Hugs_ForkThread a b))	= Hugs_ForkThread (Hugs_Catch a f1 f2 s) b
hugs_catchHugs_catch1	f1 s f2 (Right (Hugs_YieldThread a))	= Hugs_YieldThread (Hugs_Catch a f1 f2 s)
hugs_catchHugs_catch1	f1 s f2 (Right (Hugs_BlockThread a b))	= Hugs_BlockThread (hugs_catchHugs_catch0 a f1 f2 s) b
hugs_catchHugs_catch1	f1 s f2 (Right r)	= r